T:Type, f:(TT).
Inj(T;T;f)  (x, y:T. x is f*(y)  (z:T. x is f*(z)  (z is f*(y)  y is f*(z)))) 

latex

Definitions	t  T, x:AB(x), Type, Inj(A;B;f), f(a), s = t, , <a, b>, P  Q, x:A. B(x), A, , y is f*(x), Void, False, left + right, P  Q, x:A  B(x), x:A. B(x), hd(l), y=f*(x) via L, Dec(P), P & Q, P  Q, a < b, A  B, b, b | a, a ~ b, a  b, a <p b, a < b, A c B, x f y, xL. P(x), (xL.P(x)), type List, (x  l), {T}, x.A(x), x,y. t(x;y), ||as||, #$n, , i  j , l[i], s ~ t, SQType(T), y = f+(x)
Lemmas	strict-fun-connected-step, false wf, strict-fun-connected wf, fun-connected transitivity, fun-connected weakening, guard wf, fun-path wf, hd wf, length wf1, fun-path-cons, decidable lt, inject wf, fun-connected-induction, fun-connected wf, not wf